1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro
5
6 Outer measures -- overapproximations of measures
7 -/
8
9 import algebra.big_operators algebra.module
src └───────────────────┘ └────────────┘
10 topology.instances.ennreal analysis.specific_limits
src └────────────────────────┘ └──────────────────────┘
11 measure_theory.measurable_space
src └─────────────────────────────┘
12
13 noncomputable theory
14
15 open set lattice finset function filter encodable
16 open_locale classical
17
18 namespace measure_theory
19
20 structure outer_measure (α : Type*) :=
21 (measure_of : set α → ennreal)
22 (empty : measure_of ∅ = 0)
23 (mono : ∀{s₁ s₂}, s₁ ⊆ s₂ → measure_of s₁ ≤ measure_of s₂)
24 (Union_nat : ∀(s:ℕ → set α), measure_of (⋃i, s i) ≤ (∑i, measure_of (s i)))
25
26 namespace outer_measure
27
28 instance {α} : has_coe_to_fun (outer_measure α) := ⟨_, λ m, m.measure_of⟩
id └────────────┘ └───────────┘ ┴ ┴ ┴└─────────┘
src └────────────┘ └───────────┘ └─────────┘
typ └────────────┘ └───────────┘ ┴ ┴ ┴└─────────┘
29
30 section basic
31 variables {α : Type*} {ms : set (outer_measure α)} {m : outer_measure α}
id └─┘ └───────────┘ └───────────┘
src └─┘ └───────────┘ └───────────┘
typ └─┘ └───────────┘ └───────────┘
32
33 @[simp] theorem empty' (m : outer_measure α) : m ∅ = 0 := m.empty
id └───────────┘ ┴ ┴ ┴ ┴ ┴└────┘
src └───────────┘ ┴ ┴ └────┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴└────┘
doc └──┘
34
35 theorem mono' (m : outer_measure α) {s₁ s₂}
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
36 (h : s₁ ⊆ s₂) : m s₁ ≤ m s₂ := m.mono h
id └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴└───┘ ┴
src ┴ ┴ └───┘
typ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴└───┘ ┴
37
38 theorem Union_aux (m : set α → ennreal) (m0 : m ∅ = 0)
id └─┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ ┴ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘
39 {β} [encodable β] (s : β → set α) :
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
40 (∑ b, m (s b)) = ∑ i, m (⋃ b ∈ decode2 β i, s b) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
41 begin
42 have H : ∀ n, m (⋃ b ∈ decode2 β n, s b) ≠ 0 → (decode2 β n).is_some,
src └───────┘ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └───────┘
typ └───────┘ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └───────┘
doc └───────┘ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └───────┘
txt └───────┘ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └───────┘
par └───────┘ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └───────┘
pid └────┘└─┘ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └──────┘┴
43 { intros n h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
44 cases decode2 β n with b,
src └────┘ ┴ ┴ └─────┘
typ └────┘ ┴ ┴ └─────┘
doc └────┘ ┴ ┴ └─────┘
txt └────┘ ┴ ┴ └─────┘
par └────┘ ┴ ┴ └─────┘
pid ┴ ┴ ┴ └─────┘
45 { exact (h (by simp [m0])).elim },
src └────┘ ┴ ┴└────┘ ┴└──────┘
typ └────┘ ┴ ┴└────┘ ┴└──────┘
doc └────┘ ┴ ┴└────┘ ┴└──────┘
txt └────┘ ┴ ┴└────┘ ┴└──────┘
par └────┘ ┴ ┴└────┘ ┴└──────┘
pid ┴ ┴ └─────┘ └─────┘└┘
46 { exact rfl } },
id └─┘
src └────┘└─┘┴
typ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st └────────────┘└──┘└
47 refine tsum_eq_tsum_of_ne_zero_bij (λ n h, option.get (H n h)) _ _ _,
id └─────────────────────────┘ └────────┘ ┴
src └─────┘└─────────────────────────┘┴ └────┘└────────┘┴ ┴ ┴ └──────┘
typ └─────┘└─────────────────────────┘┴ └────┘└────────┘┴ ┴┴ ┴ └──────┘
doc └─────┘ ┴ └────┘ ┴ ┴ ┴ └──────┘
txt └─────┘ ┴ └────┘ ┴ ┴ ┴ └──────┘
par └─────┘ ┴ └────┘ ┴ ┴ ┴ └──────┘
pid ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘
st ─────────────────────────────────────────────────────────────────────┘└─
48 { intros m n hm hn e,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └──────────┘
st ───┘└────────────────┘└─
49 have := mem_decode2.1 (option.get_mem (H n hn)),
id └─────────┘ └────────────┘ ┴ ┴ └┘
src └──────┘└─────────┘└─┘ └────────────┘┴ ┴ ┴ └┘
typ └──────┘└─────────┘└─┘ └────────────┘┴ ┴┴┴┴└┘└┘
doc └──────┘ └─┘ ┴ ┴ ┴ └┘
txt └──────┘ └─┘ ┴ ┴ ┴ └┘
par └──────┘ └─┘ ┴ ┴ ┴ └┘
pid └───┘└─┘ └─┘ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────┘└─
50 rwa [← e, mem_decode2.1 (option.get_mem (H m hm))] at this },
id ┴ └─────────┘ └────────────┘ ┴ ┴ └┘
src └─────┘ └┘└─────────┘└─┘ └────────────┘┴ ┴ ┴ └──────────┘
typ └─────┘┴└┘└─────────┘└─┘ └────────────┘┴ ┴┴┴┴└┘└──────────┘
doc └─────┘ └┘ └─┘ ┴ ┴ ┴ └──────────┘
txt └─────┘ └┘ └─┘ ┴ ┴ ┴ └──────────┘
par └─────┘ └┘ └─┘ ┴ ┴ ┴ └──────────┘
pid └──┘ └┘ └─┘ ┴ ┴ ┴ └─┘└──────┘┴
st ───────────┘└───────────────────────────────────────┘┴└───────┘└┘└
51 { intros b h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ───┘└────────┘└─
52 refine ⟨encode b, _, _⟩,
id └────┘ ┴
src └─────┘ └────┘┴ └─────┘
typ └─────┘ └────┘┴┴└─────┘
doc └─────┘ ┴ └─────┘
txt └─────┘ ┴ └─────┘
par └─────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ──────────────────────────┘└─
53 { convert h, simp [ext_iff, encodek2] },
id ┴ └─────┘ └──────┘
src └──────┘ └────┘└─────┘└┘└──────┘└┘
typ └──────┘┴ └────┘└─────┘└┘└──────┘└┘
doc └──────┘ └────┘ └┘ └┘
txt └──────┘ └────┘ └┘ └┘
par └──────┘ └────┘ └┘ └┘
pid ┴ ┴┴ └┘ ┴┴
st ─────┘└───────┘└─────────────────────────┘└┘└
54 { exact option.get_of_mem _ (encodek2 _) } },
id └───────────────┘ └──────┘
src └────┘└───────────────┘└─┘ └──────┘└──┘
typ └────┘└───────────────┘└─┘ └──────┘└──┘
doc └────┘ └─┘ └──┘
txt └────┘ └─┘ └──┘
par └────┘ └─┘ └──┘
pid ┴ └─┘ └─┘┴
st ────────────────────────────────────────────┘└──┘└
55 { intros n h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────────────┘└─
56 transitivity, swap,
src └──────────┘ └──┘
typ └──────────┘ └──┘
doc └──────────┘ └──┘
txt └──────────┘ └──┘
par └──────────┘ └──┘
st ───────────────┘└────┘└─
57 rw [show decode2 β n = _, from option.get_mem (H n h)],
id └─────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴
src └──┘ ┴└─────┘┴ ┴ ┴┴└───────┘└────────────┘┴ ┴ ┴ └┘
typ └──┘ ┴└─────┘┴┴┴ ┴┴└───────┘└────────────┘┴ ┴┴┴┴┴└┘
doc └──┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘
txt └──┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘
par └──┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘
pid └┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────────────┘└──
58 congr, simp [ext_iff, -option.some_get] }
id └─────┘
src └───┘ └────┘└─────┘└──────────────────┘
typ └───┘ └────┘└─────┘└──────────────────┘
doc └────┘ └──────────────────┘
txt └───┘ └────┘ └──────────────────┘
par └───┘ └────┘ └──────────────────┘
pid ┴┴ └─────────────────┘┴
st ────────┘└─────────────────────────────────┘└─
59 end
st ──┘
60
61 protected theorem Union (m : outer_measure α)
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
62 {β} [encodable β] (s : β → set α) :
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
63 m (⋃i, s i) ≤ (∑i, m (s i)) :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
64 by rw [Union_decode2, Union_aux _ m.empty' s]; exact m.Union_nat _
id └───────────┘ └───────┘ └──────┘ ┴ └─────────┘
src └──┘└───────────┘└┘└───────┘└─┘└──────┘┴ ┴ └────┘└─────────┘└──
typ └──┘└───────────┘└┘└───────┘└─┘└──────┘┴┴┴ └────┘└─────────┘└──
doc └──┘ └┘ └─┘ ┴ ┴ └────┘ └──
txt └──┘ └┘ └─┘ ┴ ┴ └────┘ └──
par └──┘ └┘ └─┘ ┴ ┴ └────┘ └──
pid └┘ └┘ └─┘ ┴ ┴ ┴ └┘└
st └────────────────┘└──────────────────────┘┴└─────────────────────
65
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
66 lemma Union_null (m : outer_measure α)
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
67 {β} [encodable β] {s : β → set α} (h : ∀ i, m (s i) = 0) : m (⋃i, s i) = 0 :=
id └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc └───────┘ ┴ ┴
68 by simpa [h] using m.Union s
id ┴ └─────┘ ┴
src └─────┘ └──────┘└─────┘┴ └
typ └─────┘┴└──────┘└─────┘┴┴└
doc └─────┘ └──────┘ ┴ └
txt └─────┘ └──────┘ ┴ └
par └─────┘ └──────┘ ┴ └
pid ┴┴ ┴┴└────┘ ┴ └
st └──────────────────────────
69
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
70 protected lemma union (m : outer_measure α) (s₁ s₂ : set α) :
id └───────────┘ ┴ └─┘ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴
71 m (s₁ ∪ s₂) ≤ m s₁ + m s₂ :=
id ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
src ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
72 begin
st └─────
73 convert m.Union (λ b, cond b s₁ s₂),
id └─────┘ └──┘ └┘ └┘
src └──────┘└─────┘┴ └──┘└──┘┴ ┴ ┴ ┴
typ └──────┘└─────┘┴ └──┘└──┘┴ ┴└┘┴└┘┴
doc └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴
txt └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴
par └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴
pid ┴ ┴ └──┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────┘└─
74 { simp [union_eq_Union] },
id └────────────┘
src └────┘└────────────┘└┘
typ └────┘└────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───┘└────────────────────┘└┘└
75 { rw tsum_fintype, change _ = _ + _, simp }
id └──────────┘ ┴ ┴
src └─┘└──────────┘ └───────┘┴└─┘┴└┘ └───┘
typ └─┘└──────────┘ └───────┘┴└─┘┴└┘ └───┘
doc └─┘ └───────┘ └─┘ └┘ └───┘
txt └─┘ └───────┘ └─┘ └┘ └───┘
par └─┘ └───────┘ └─┘ └┘ └───┘
pid ┴ └─┘ └─┘ └┘ ┴
st ──────────────────┘└────────────────┘└─────┘└─
76 end
st ──┘
77
78 lemma union_null (m : outer_measure α) {s₁ s₂ : set α}
id └───────────┘ ┴ └─┘ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴
79 (h₁ : m s₁ = 0) (h₂ : m s₂ = 0) : m (s₁ ∪ s₂) = 0 :=
id ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴
src ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴
80 by simpa [h₁, h₂] using m.union s₁ s₂
id └┘ └┘ └─────┘ └┘ └┘
src └─────┘ └┘ └──────┘└─────┘┴ ┴ └
typ └─────┘└┘└┘└┘└──────┘└─────┘┴└┘┴└┘└
doc └─────┘ └┘ └──────┘ ┴ ┴ └
txt └─────┘ └┘ └──────┘ ┴ ┴ └
par └─────┘ └┘ └──────┘ ┴ ┴ └
pid ┴┴ └┘ ┴┴└────┘ ┴ ┴ └
st └───────────────────────────────────
81
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
82 @[ext] lemma ext : ∀{μ₁ μ₂ : outer_measure α},
id ┴ └───────────┘ ┴
src └───────────┘
typ ┴ └───────────┘ ┴
doc └─┘
83 (∀s, μ₁ s = μ₂ s) → μ₁ = μ₂
id ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘
84 | ⟨m₁, e₁, _, u₁⟩ ⟨m₂, e₂, _, u₂⟩ h := by congr; exact funext h
id └────┘ ┴
src └───┘ └────┘└────┘┴ └
typ └───┘ └────┘└────┘┴┴└
doc └────┘ ┴ └
txt └───┘ └────┘ ┴ └
par └───┘ └────┘ ┴ └
pid ┴ ┴ └
st └──────────────────────
85
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
86 instance : has_zero (outer_measure α) :=
id └──────┘ └───────────┘ ┴
src └──────┘ └───────────┘
typ └──────┘ └───────────┘ ┴
87 ⟨{ measure_of := λ_, 0,
id ┴
typ ┴
88 empty := rfl,
id └─┘
src └─┘
typ └─┘
89 mono := assume _ _ _, le_refl 0,
id ┴ ┴ ┴ └─────┘
src └─────┘
typ ┴ ┴ ┴ └─────┘
90 Union_nat := assume s, zero_le _ }⟩
id ┴ └─────┘
src └─────┘
typ ┴ └─────┘
91
92 @[simp] theorem zero_apply (s : set α) : (0 : outer_measure α) s = 0 := rfl
id └─┘ ┴ └───────────┘ ┴ ┴ ┴ └─┘
src └─┘ └───────────┘ ┴ └─┘
typ └─┘ ┴ └───────────┘ ┴ ┴ ┴ └─┘
doc └──┘
93
94 instance : inhabited (outer_measure α) := ⟨0⟩
id └───────┘ └───────────┘ ┴
src └───────┘ └───────────┘
typ └───────┘ └───────────┘ ┴
95
96 instance : has_add (outer_measure α) :=
id └─────┘ └───────────┘ ┴
src └─────┘ └───────────┘
typ └─────┘ └───────────┘ ┴
97 ⟨λm₁ m₂,
id └┘ └┘
typ └┘ └┘
98 { measure_of := λs, m₁ s + m₂ s,
id ┴ └┘ ┴ ┴ └┘ ┴
src ┴
typ ┴ └┘ ┴ ┴ └┘ ┴
99 empty := show m₁ ∅ + m₂ ∅ = 0, by simp [outer_measure.empty],
id └┘ ┴ ┴ └┘ ┴ ┴ └─────────────────┘
src ┴ ┴ ┴ ┴ └────┘└─────────────────┘┴
typ └┘ ┴ ┴ └┘ ┴ ┴ └────┘└─────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────────────┘
100 mono := assume s₁ s₂ h, add_le_add' (m₁.mono h) (m₂.mono h),
id └┘ └┘ ┴ └─────────┘ └┘└───┘ ┴ └┘└───┘ ┴
src └─────────┘ └───┘ └───┘
typ └┘ └┘ ┴ └─────────┘ └┘└───┘ ┴ └┘└───┘ ┴
101 Union_nat := assume s,
id ┴
typ ┴
102 calc m₁ (⋃i, s i) + m₂ (⋃i, s i) ≤
id └┘ ┴┴┴ ┴ ┴ ┴ └┘ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ └┘ ┴┴┴ ┴ ┴ ┴ └┘ ┴┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
103 (∑i, m₁ (s i)) + (∑i, m₂ (s i)) :
id ┴┴┴ └┘ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ └┘ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴
doc ┴ ┴ ┴ ┴
104 add_le_add' (m₁.Union_nat s) (m₂.Union_nat s)
id └─────────┘ └┘└────────┘ ┴ └┘└────────┘ ┴
src └─────────┘ └────────┘ └────────┘
typ └─────────┘ └┘└────────┘ ┴ └┘└────────┘ ┴
105 ... = _ : ennreal.tsum_add.symm}⟩
id └──────────────┘└───┘
src └──────────────┘└───┘
typ └──────────────┘└───┘
st ┴
106
107 @[simp] theorem add_apply (m₁ m₂ : outer_measure α) (s : set α) :
id └───────────┘ ┴ └─┘ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴
doc └──┘
108 (m₁ + m₂) s = m₁ s + m₂ s := rfl
id └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘
109
110 instance add_comm_monoid : add_comm_monoid (outer_measure α) :=
id └─────────────┘ └───────────┘ ┴
src └─────────────┘ └───────────┘
typ └─────────────┘ └───────────┘ ┴
111 { zero := 0,
112 add := (+),
id ┴
src ┴
typ ┴
113 add_comm := assume a b, ext $ assume s, add_comm _ _,
id ┴ ┴ └─┘ ┴ └──────┘
src └─┘ └──────┘
typ ┴ ┴ └─┘ ┴ └──────┘
114 add_assoc := assume a b c, ext $ assume s, add_assoc _ _ _,
id ┴ ┴ ┴ └─┘ ┴ └───────┘
src └─┘ └───────┘
typ ┴ ┴ ┴ └─┘ ┴ └───────┘
115 add_zero := assume a, ext $ assume s, add_zero _,
id ┴ └─┘ ┴ └──────┘
src └─┘ └──────┘
typ ┴ └─┘ ┴ └──────┘
116 zero_add := assume a, ext $ assume s, zero_add _ }
id ┴ └─┘ ┴ └──────┘
src └─┘ └──────┘
typ ┴ └─┘ ┴ └──────┘
117
118 instance : has_bot (outer_measure α) := ⟨0⟩
id └─────┘ └───────────┘ ┴
src └─────┘ └───────────┘
typ └─────┘ └───────────┘ ┴
doc └─────┘
119
120 instance outer_measure.order_bot : order_bot (outer_measure α) :=
id └───────┘ └───────────┘ ┴
src └───────┘ └───────────┘
typ └───────┘ └───────────┘ ┴
doc └───────┘
121 { le := λm₁ m₂, ∀s, m₁ s ≤ m₂ s,
id ┴ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ ┴
typ ┴ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴
122 bot := 0,
123 le_refl := assume a s, le_refl _,
id ┴ ┴ └─────┘
src └─────┘
typ ┴ ┴ └─────┘
124 le_trans := assume a b c hab hbc s, le_trans (hab s) (hbc s),
id ┴ ┴ ┴ └─┘ └─┘ ┴ └──────┘ └─┘ ┴ └─┘ ┴
src └──────┘
typ ┴ ┴ ┴ └─┘ └─┘ ┴ └──────┘ └─┘ ┴ └─┘ ┴
125 le_antisymm := assume a b hab hba, ext $ assume s, le_antisymm (hab s) (hba s),
id ┴ ┴ └─┘ └─┘ └─┘ ┴ └─────────┘ └─┘ ┴ └─┘ ┴
src └─┘ └─────────┘
typ ┴ ┴ └─┘ └─┘ └─┘ ┴ └─────────┘ └─┘ ┴ └─┘ ┴
126 bot_le := assume a s, zero_le _ }
id ┴ ┴ └─────┘
src └─────┘
typ ┴ ┴ └─────┘
127
128 section supremum
129
130 instance : has_Sup (outer_measure α) :=
id └─────┘ └───────────┘ ┴
src └─────┘ └───────────┘
typ └─────┘ └───────────┘ ┴
doc └─────┘
131 ⟨λms, {
id └┘
typ └┘
132 measure_of := λs, ⨆m:ms, m.val s,
id ┴ ┴ └┘┴ ┴└──┘ ┴
src ┴ ┴ └──┘
typ ┴ ┴ └┘┴ ┴└──┘ ┴
doc ┴ ┴
133 empty := le_zero_iff_eq.1 $ supr_le $ λ ⟨m, h⟩, le_of_eq m.empty,
id └────────────┘┴ └─────┘ ┴┴ └──────┘ └────┘
src └────────────┘┴ └─────┘ └──────┘ └────┘
typ └────────────┘┴ └─────┘ ┴┴ └──────┘ └────┘
134 mono := assume s₁ s₂ hs, supr_le_supr $ assume ⟨m, hm⟩, m.mono hs,
id └┘ └┘ └┘ └──────────┘ ┴┴ └───┘ └┘
src └──────────┘ └───┘
typ └┘ └┘ └┘ └──────────┘ ┴┴ └───┘ └┘
135 Union_nat := assume f, supr_le $ assume m,
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
136 calc m.val (⋃i, f i) ≤ (∑ (i : ℕ), m.val (f i)) : m.val.Union_nat _
id ┴└──┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘└────────┘
src └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘└────────┘
typ ┴└──┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘└────────┘
doc ┴ ┴ ┴ ┴
137 ... ≤ (∑i, ⨆m:ms, m.val (f i)) :
id ┴┴┴ ┴ └┘┴ ┴└──┘ ┴ ┴
src ┴ ┴ ┴ ┴ └──┘
typ ┴┴┴ ┴ └┘┴ ┴└──┘ ┴ ┴
doc ┴ ┴ ┴ ┴
138 ennreal.tsum_le_tsum $ assume i, le_supr (λm:ms, m.val (f i)) m }⟩
id └──────────────────┘ ┴ └─────┘ └┘ ┴└──┘ ┴ ┴ ┴
src └──────────────────┘ └─────┘ └──┘
typ └──────────────────┘ ┴ └─────┘ └┘ ┴└──┘ ┴ ┴ ┴
139
140 private lemma le_Sup (hm : m ∈ ms) : m ≤ Sup ms :=
id ┴ ┴ └┘ ┴ ┴ └─┘ └┘
src ┴ ┴ └─┘
typ ┴ ┴ └┘ ┴ ┴ └─┘ └┘
doc └─┘
141 λ s, le_supr (λm:ms, m.val s) ⟨m, hm⟩
id ┴ └─────┘ └┘ ┴└──┘ ┴ ┴ └┘
src └─────┘ └──┘
typ ┴ └─────┘ └┘ ┴└──┘ ┴ ┴ └┘
142
143 private lemma Sup_le (hm : ∀m' ∈ ms, m' ≤ m) : Sup ms ≤ m :=
id └┘ └┘ └┘ ┴ ┴ └─┘ └┘ ┴ ┴
src └┘ ┴ └─┘ ┴
typ └┘ └┘ └┘ ┴ ┴ └─┘ └┘ ┴ ┴
doc └─┘
144 λ s, (supr_le $ assume ⟨m', h'⟩, (hm m' h') s)
id ┴ └─────┘ ┴└┘ └┘ └┘ ┴
src └─────┘
typ ┴ └─────┘ ┴└┘ └┘ └┘ ┴
145
146 instance : has_Inf (outer_measure α) := ⟨λs, Sup {m | ∀m'∈s, m ≤ m'}⟩
id └─────┘ └───────────┘ ┴ ┴ └─┘ ┴┴ └┘ ┴ ┴ ┴ └┘
src └─────┘ └───────────┘ └─┘ ┴ ┴
typ └─────┘ └───────────┘ ┴ ┴ └─┘ ┴┴ └┘ ┴ ┴ ┴ └┘
doc └─────┘ └─┘
147 private lemma Inf_le (hm : m ∈ ms) : Inf ms ≤ m := Sup_le $ assume m' h', h' _ hm
id ┴ ┴ └┘ └─┘ └┘ ┴ ┴ └────┘ └┘ └┘ └┘ └┘
src ┴ └─┘ ┴ └────┘
typ ┴ ┴ └┘ └─┘ └┘ ┴ ┴ └────┘ └┘ └┘ └┘ └┘
doc └─┘
148 private lemma le_Inf (hm : ∀m' ∈ ms, m ≤ m') : m ≤ Inf ms := le_Sup hm
id └┘ └┘ ┴ ┴ └┘ ┴ ┴ └─┘ └┘ └────┘ └┘
src ┴ ┴ └─┘ └────┘
typ └┘ └┘ ┴ ┴ └┘ ┴ ┴ └─┘ └┘ └────┘ └┘
doc └─┘
149
150 instance : complete_lattice (outer_measure α) :=
id └──────────────┘ └───────────┘ ┴
src └──────────────┘ └───────────┘
typ └──────────────┘ └───────────┘ ┴
doc └──────────────┘
151 { top := Sup univ,
id └─┘ └──┘
src └─┘ └──┘
typ └─┘ └──┘
doc └─┘
152 le_top := assume a, le_Sup (mem_univ a),
id ┴ └────┘ └──────┘ ┴
src └────┘ └──────┘
typ ┴ └────┘ └──────┘ ┴
153 Sup := Sup,
id └─┘
src └─┘
typ └─┘
doc └─┘
154 Sup_le := assume s m, Sup_le,
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
155 le_Sup := assume s m, le_Sup,
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
156 Inf := Inf,
id └─┘
src └─┘
typ └─┘
doc └─┘
157 Inf_le := assume s m, Inf_le,
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
158 le_Inf := assume s m, le_Inf,
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
159 sup := λa b, Sup {a, b},
id ┴ ┴ └─┘ ┴┴┴ ┴
src └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴┴┴ ┴
doc └─┘
160 le_sup_left := assume a b, le_Sup $ by simp,
id ┴ ┴ └────┘
src └────┘ └──┘
typ ┴ ┴ └────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
161 le_sup_right := assume a b, le_Sup $ by simp,
id ┴ ┴ └────┘
src └────┘ └──┘
typ ┴ ┴ └────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
162 sup_le := assume a b c ha hb, Sup_le $ by simp [or_imp_distrib, ha, hb] {contextual:=tt},
id ┴ ┴ ┴ └┘ └┘ └────┘ └────────────┘ └┘ └┘ └┘
src └────┘ └────┘└────────────┘└┘ └┘ └┘ └──────────┘└┘┴
typ ┴ ┴ ┴ └┘ └┘ └────┘ └────┘└────────────┘└┘└┘└┘└┘└┘ └──────────┘└┘┴
doc └────┘ └┘ └┘ └┘ └──────────┘ ┴
txt └────┘ └┘ └┘ └┘ └──────────┘ ┴
par └────┘ └┘ └┘ └┘ └──────────┘ ┴
pid ┴┴ └┘ └┘ ┴┴ └──────────┘ ┴
st └─────────────────────────────────────────────┘
163 inf := λa b, Inf {a, b},
id ┴ ┴ └─┘ ┴┴┴ ┴
src └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴┴┴ ┴
doc └─┘
164 inf_le_left := assume a b, Inf_le $ by simp,
id ┴ ┴ └────┘
src └────┘ └──┘
typ ┴ ┴ └────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
165 inf_le_right := assume a b, Inf_le $ by simp,
id ┴ ┴ └────┘
src └────┘ └──┘
typ ┴ ┴ └────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
166 le_inf := assume a b c ha hb, le_Inf $ by simp [or_imp_distrib, ha, hb] {contextual:=tt},
id ┴ ┴ ┴ └┘ └┘ └────┘ └────────────┘ └┘ └┘ └┘
src └────┘ └────┘└────────────┘└┘ └┘ └┘ └──────────┘└┘┴
typ ┴ ┴ ┴ └┘ └┘ └────┘ └────┘└────────────┘└┘└┘└┘└┘└┘ └──────────┘└┘┴
doc └────┘ └┘ └┘ └┘ └──────────┘ ┴
txt └────┘ └┘ └┘ └┘ └──────────┘ ┴
par └────┘ └┘ └┘ └┘ └──────────┘ ┴
pid ┴┴ └┘ └┘ ┴┴ └──────────┘ ┴
st └─────────────────────────────────────────────┘
167 .. outer_measure.order_bot }
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
168
169 @[simp] theorem Sup_apply (ms : set (outer_measure α)) (s : set α) :
id └─┘ └───────────┘ ┴ └─┘ ┴
src └─┘ └───────────┘ └─┘
typ └─┘ └───────────┘ ┴ └─┘ ┴
doc └──┘
170 (Sup ms) s = ⨆ m : ms, m s := rfl
id └─┘ └┘ ┴ ┴ ┴ └┘┴ ┴ ┴ └─┘
src └─┘ ┴ ┴ ┴ └─┘
typ └─┘ └┘ ┴ ┴ ┴ └┘┴ ┴ ┴ └─┘
doc └─┘ ┴ ┴
171
172 @[simp] theorem supr_apply {ι} (f : ι → outer_measure α) (s : set α) :
id ┴ └───────────┘ ┴ └─┘ ┴
src └───────────┘ └─┘
typ ┴ └───────────┘ ┴ └─┘ ┴
doc └──┘
173 (⨆ i : ι, f i) s = ⨆ i, f i s :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
174 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
175 (supr_le $ λ ⟨_, i, rfl⟩, le_supr _ i)
id └─────┘ ┴ ┴ └─┘ └─────┘
src └─────┘ └─┘ └─────┘
typ └─────┘ ┴ ┴ └─┘ └─────┘
176 (supr_le $ λ i, le_supr
id └─────┘ ┴ └─────┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘
177 (λ (m : {a : outer_measure α // ∃ i, f i = a}), m.1 s)
id ┴ └───────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ └───────────┘ ┴ ┴ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴
178 ⟨f i, i, rfl⟩)
id ┴ ┴ ┴ └─┘
src └─┘
typ ┴ ┴ ┴ └─┘
179
180 @[simp] theorem sup_apply (m₁ m₂ : outer_measure α) (s : set α) :
id └───────────┘ ┴ └─┘ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴
doc └──┘
181 (m₁ ⊔ m₂) s = m₁ s ⊔ m₂ s :=
id └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
182 by have := supr_apply (λ b, cond b m₁ m₂) s;
id └────────┘ └──┘ └┘ └┘ ┴
src └──────┘└────────┘┴ └──┘└──┘┴ ┴ ┴ └┘
typ └──────┘└────────┘┴ └──┘└──┘┴ ┴└┘┴└┘└┘┴
doc └──────┘ ┴ └──┘ ┴ ┴ ┴ └┘
txt └──────┘ ┴ └──┘ ┴ ┴ ┴ └┘
par └──────┘ ┴ └──┘ ┴ ┴ ┴ └┘
pid └───┘└─┘ ┴ └──┘ ┴ ┴ ┴ └┘
st └──────────────────────────────────────────
183 rwa [supr_bool_eq, supr_bool_eq] at this
id └──────────┘ └──────────┘
src └───┘└──────────┘└┘└──────────┘└─────────
typ └───┘└──────────┘└┘└──────────┘└─────────
doc └───┘ └┘ └─────────
txt └───┘ └┘ └─────────
par └───┘ └┘ └─────────
pid └┘ └┘ ┴└──────┘└
st ──────┘└──────────┘└────────────┘┴└────────
184
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
185 end supremum
186
187 def map {β} (f : α → β) (m : outer_measure α) : outer_measure β :=
id ┴ ┴ └───────────┘ ┴ └───────────┘ ┴
src └───────────┘ └───────────┘
typ ┴ ┴ └───────────┘ ┴ └───────────┘ ┴
188 { measure_of := λs, m (f ⁻¹' s),
id ┴ ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ ┴ └─┘ ┴
doc └─┘
189 empty := m.empty,
id ┴└────┘
src └────┘
typ ┴└────┘
190 mono := λ s t h, m.mono (preimage_mono h),
id ┴ ┴ ┴ ┴└───┘ └───────────┘ ┴
src └───┘ └───────────┘
typ ┴ ┴ ┴ ┴└───┘ └───────────┘ ┴
191 Union_nat := λ s, by rw [preimage_Union]; exact
id ┴ └────────────┘
src └──┘└────────────┘┴ └─────
typ ┴ └──┘└────────────┘┴ └─────
doc └──┘ ┴ └─────
txt └──┘ ┴ └─────
par └──┘ ┴ └─────
pid └┘ ┴ └
st └─────────────────┘┴└───────
192 m.Union_nat (λ i, f ⁻¹' s i) }
id └─────────┘ ┴ └─┘ ┴
src ───┘└─────────┘┴ └──┘ ┴└─┘┴ ┴ └┘
typ ───┘└─────────┘┴ └──┘┴┴└─┘┴┴┴ └┘
doc ───┘ ┴ └──┘ ┴└─┘┴ ┴ └┘
txt ───┘ ┴ └──┘ ┴ ┴ ┴ └┘
par ───┘ ┴ └──┘ ┴ ┴ ┴ └┘
pid ───┘ ┴ └──┘ ┴ ┴ ┴ ┴┴
st ────────────────────────────────┘
193
194 @[simp] theorem map_apply {β} (f : α → β)
id ┴ ┴
typ ┴ ┴
doc └──┘
195 (m : outer_measure α) (s : set β) : map f m s = m (f ⁻¹' s) := rfl
id └───────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘
src └───────────┘ └─┘ └─┘ ┴ └─┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘
doc └─┘
196
197 @[simp] theorem map_id (m : outer_measure α) : map id m = m :=
id └───────────┘ ┴ └─┘ └┘ ┴ ┴ ┴
src └───────────┘ └─┘ └┘ ┴
typ └───────────┘ ┴ └─┘ └┘ ┴ ┴ ┴
doc └──┘
198 ext $ λ s, rfl
id └─┘ ┴ └─┘
src └─┘ └─┘
typ └─┘ ┴ └─┘
199
200 @[simp] theorem map_map {β γ} (f : α → β) (g : β → γ)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
201 (m : outer_measure α) : map g (map f m) = map (g ∘ f) m :=
id └───────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └───────────┘ └─┘ └─┘ ┴ └─┘ ┴
typ └───────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
202 ext $ λ s, rfl
id └─┘ ┴ └─┘
src └─┘ └─┘
typ └─┘ ┴ └─┘
203
204 instance : functor outer_measure := {map := λ α β, map}
id └─────┘ └───────────┘ ┴ ┴ └─┘
src └─────┘ └───────────┘ └─┘
typ └─────┘ └───────────┘ ┴ ┴ └─┘
205
206 instance : is_lawful_functor outer_measure :=
id └───────────────┘ └───────────┘
src └───────────────┘ └───────────┘
typ └───────────────┘ └───────────┘
207 { id_map := λ α, map_id,
id ┴ ┴ └────┘
src ┴ └────┘
typ ┴ ┴ └────┘
208 comp_map := λ α β γ f g m, (map_map f g m).symm }
id ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘
src └─────┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘
209
210 /-- The dirac outer measure. -/
211 def dirac (a : α) : outer_measure α :=
id ┴ └───────────┘ ┴
src └───────────┘
typ ┴ └───────────┘ ┴
212 { measure_of := λs, ⨆ h : a ∈ s, 1,
id ┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴
doc ┴ ┴
213 empty := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
214 mono := λ s t h, supr_le_supr2 (λ h', ⟨h h', le_refl _⟩),
id ┴ ┴ ┴ └───────────┘ └┘ ┴ └┘ └─────┘
src └───────────┘ └─────┘
typ ┴ ┴ ┴ └───────────┘ └┘ ┴ └┘ └─────┘
215 Union_nat := λ s, supr_le $ λ h,
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
216 let ⟨i, h⟩ := mem_Union.1 h in
id └─┘ ┴ └───────┘┴ ┴
src └───────┘┴
typ └─┘ ┴ └───────┘┴ ┴
217 le_trans (by exact le_supr _ h) (ennreal.le_tsum i) }
id └──────┘ └─────┘ ┴ └─────────────┘
src └──────┘ └────┘└─────┘└─┘ └─────────────┘
typ └──────┘ └────┘└─────┘└─┘┴ └─────────────┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st └────────────────┘
218
219 @[simp] theorem dirac_apply (a : α) (s : set α) :
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
doc └──┘
220 dirac a s = ⨆ h : a ∈ s, 1 := rfl
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─┘
src └───┘ ┴ ┴ ┴ ┴ └─┘
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─┘
doc └───┘ ┴ ┴
221
222 def sum {ι} (f : ι → outer_measure α) : outer_measure α :=
id ┴ └───────────┘ ┴ └───────────┘ ┴
src └───────────┘ └───────────┘
typ ┴ └───────────┘ ┴ └───────────┘ ┴
223 { measure_of := λs, ∑ i, f i s,
id ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴
224 empty := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
225 mono := λ s t h, ennreal.tsum_le_tsum (λ i, (f i).mono' h),
id ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴ └───┘ ┴
src └──────────────────┘ └───┘
typ ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴ └───┘ ┴
226 Union_nat := λ s, by rw ennreal.tsum_comm; exact
id ┴ └───────────────┘
src └─┘└───────────────┘ └─────
typ ┴ └─┘└───────────────┘ └─────
doc └─┘ └─────
txt └─┘ └─────
par └─┘ └─────
pid ┴ └
st └────────────────────────────
227 ennreal.tsum_le_tsum (λ i, (f i).Union_nat _) }
id └──────────────────┘ ┴
src ───┘└──────────────────┘┴ └──┘ ┴ └─────────────┘
typ ───┘└──────────────────┘┴ └──┘ ┴┴ └─────────────┘
doc ───┘ ┴ └──┘ ┴ └─────────────┘
txt ───┘ ┴ └──┘ ┴ └─────────────┘
par ───┘ ┴ └──┘ ┴ └─────────────┘
pid ───┘ ┴ └──┘ ┴ └────────────┘┴
st ─────────────────────────────────────────────────┘
228
229 @[simp] theorem sum_apply {ι} (f : ι → outer_measure α) (s : set α) :
id ┴ └───────────┘ ┴ └─┘ ┴
src └───────────┘ └─┘
typ ┴ └───────────┘ ┴ └─┘ ┴
doc └──┘
230 sum f s = ∑ i, f i s := rfl
id └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └─┘
src └─┘ ┴ ┴ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └─┘
doc ┴ ┴
231
232 instance : has_scalar ennreal (outer_measure α) :=
id └────────┘ └─────┘ └───────────┘ ┴
src └────────┘ └─────┘ └───────────┘
typ └────────┘ └─────┘ └───────────┘ ┴
doc └────────┘ └─────┘
233 ⟨λ a m, {
id ┴ ┴
typ ┴ ┴
234 measure_of := λs, a * m s,
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
235 empty := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
236 mono := λ s t h, canonically_ordered_semiring.mul_le_mul (le_refl _) (m.mono' h),
id ┴ ┴ ┴ └─────────────────────────────────────┘ └─────┘ ┴└────┘ ┴
src └─────────────────────────────────────┘ └─────┘ └────┘
typ ┴ ┴ ┴ └─────────────────────────────────────┘ └─────┘ ┴└────┘ ┴
237 Union_nat := λ s, by rw ennreal.mul_tsum; exact
id ┴ └──────────────┘
src └─┘└──────────────┘ └─────
typ ┴ └─┘└──────────────┘ └─────
doc └─┘ └─────
txt └─┘ └─────
par └─┘ └─────
pid ┴ └
st └───────────────────────────
238 canonically_ordered_semiring.mul_le_mul (le_refl _) (m.Union_nat _) }⟩
id └─────────────────────────────────────┘ └─────┘ └─────────┘
src ───┘└─────────────────────────────────────┘┴ └─────┘└──┘ └─────────┘└──┘
typ ───┘└─────────────────────────────────────┘┴ └─────┘└──┘ └─────────┘└──┘
doc ───┘ ┴ └──┘ └──┘
txt ───┘ ┴ └──┘ └──┘
par ───┘ ┴ └──┘ └──┘
pid ───┘ ┴ └──┘ └─┘┴
st ───────────────────────────────────────────────────────────────────────┘
239
240 @[simp] theorem smul_apply (a : ennreal) (m : outer_measure α) (s : set α) :
id └─────┘ └───────────┘ ┴ └─┘ ┴
src └─────┘ └───────────┘ └─┘
typ └─────┘ └───────────┘ ┴ └─┘ ┴
doc └──┘ └─────┘
241 (a • m) s = a * m s := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
242
243 instance : semimodule ennreal (outer_measure α) :=
id └────────┘ └─────┘ └───────────┘ ┴
src └────────┘ └─────┘ └───────────┘
typ └────────┘ └─────┘ └───────────┘ ┴
doc └────────┘ └─────┘
244 { smul_add := λ a m₁ m₂, ext $ λ s, mul_add _ _ _,
id ┴ └┘ └┘ └─┘ ┴ └─────┘
src └─┘ └─────┘
typ ┴ └┘ └┘ └─┘ ┴ └─────┘
245 add_smul := λ a b m, ext $ λ s, add_mul _ _ _,
id ┴ ┴ ┴ └─┘ ┴ └─────┘
src └─┘ └─────┘
typ ┴ ┴ ┴ └─┘ ┴ └─────┘
246 mul_smul := λ a b m, ext $ λ s, mul_assoc _ _ _,
id ┴ ┴ ┴ └─┘ ┴ └───────┘
src └─┘ └───────┘
typ ┴ ┴ ┴ └─┘ ┴ └───────┘
247 one_smul := λ m, ext $ λ s, one_mul _,
id ┴ └─┘ ┴ └─────┘
src └─┘ └─────┘
typ ┴ └─┘ ┴ └─────┘
248 zero_smul := λ m, ext $ λ s, zero_mul _,
id ┴ └─┘ ┴ └──────┘
src └─┘ └──────┘
typ ┴ └─┘ ┴ └──────┘
249 smul_zero := λ a, ext $ λ s, mul_zero _,
id ┴ └─┘ ┴ └──────┘
src └─┘ └──────┘
typ ┴ └─┘ ┴ └──────┘
250 ..outer_measure.has_scalar }
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
251
252 theorem smul_dirac_apply (a : ennreal) (b : α) (s : set α) :
id └─────┘ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ └─┘ ┴
doc └─────┘
253 (a • dirac b) s = ⨆ h : b ∈ s, a :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
doc └───┘ ┴ ┴
254 by by_cases b ∈ s; simp [h]
id ┴ ┴ ┴ ┴
src └───────┘ ┴┴┴ └────┘ └─
typ └───────┘┴┴┴┴┴ └────┘┴└─
doc └───────┘ ┴ ┴ └────┘ └─
txt └───────┘ ┴ ┴ └────┘ └─
par └───────┘ ┴ ┴ └────┘ └─
pid ┴ ┴ ┴ ┴┴ ┴└
st └─────────────────────────
255
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
256 theorem top_apply {s : set α} (h : s.nonempty) : (⊤ : outer_measure α) s = ⊤ :=
id └─┘ ┴ ┴└───────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
src └─┘ └───────┘ ┴ └───────────┘ ┴ ┴
typ └─┘ ┴ ┴└───────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └───────┘
257 let ⟨a, as⟩ := h in
id └─┘ ┴ ┴
typ └─┘ ┴ ┴
258 top_unique $ le_supr_of_le ⟨(⊤ : ennreal) • dirac a, trivial⟩ $
id └────────┘ └───────────┘ ┴ └─────┘ ┴ └───┘ └─────┘
src └────────┘ └───────────┘ ┴ └─────┘ ┴ └───┘ └─────┘
typ └────────┘ └───────────┘ ┴ └─────┘ ┴ └───┘ └─────┘
doc └─────┘ └───┘
259 by simp [smul_dirac_apply, as]
id └──────────────┘ └┘
src └────┘└──────────────┘└┘ └─
typ └────┘└──────────────┘└┘└┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────
260
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
261 end basic
262
263 section of_function
264 set_option eqn_compiler.zeta true
doc └───────────────┘
265
266 /-- Given any function `m` assigning measures to sets satisying `m ∅ = 0`, there is
267 a unique maximal outer measure `μ` satisfying `μ s ≤ m s` for all `s : set α`. -/
268 protected def of_function {α : Type*} (m : set α → ennreal) (m_empty : m ∅ = 0) :
id └─┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ ┴ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘
269 outer_measure α :=
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
270 let μ := λs, ⨅{f : ℕ → set α} (h : s ⊆ ⋃i, f i), ∑i, m (f i) in
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
271 { measure_of := μ,
id ┴
typ ┴
272 empty := le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
273 (infi_le_of_le (λ_, ∅) $ infi_le_of_le (empty_subset _) $ by simp [m_empty])
id └───────────┘ ┴ ┴ └───────────┘ └──────────┘ └─────┘
src └───────────┘ ┴ └───────────┘ └──────────┘ └────┘ ┴
typ └───────────┘ ┴ ┴ └───────────┘ └──────────┘ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────┘
274 (zero_le _),
id └─────┘
src └─────┘
typ └─────┘
275 mono := assume s₁ s₂ hs, infi_le_infi $ assume f,
id └┘ └┘ └┘ └──────────┘ ┴
src └──────────┘
typ └┘ └┘ └┘ └──────────┘ ┴
276 infi_le_infi2 $ assume hb, ⟨subset.trans hs hb, le_refl _⟩,
id └───────────┘ └┘ └──────────┘ └┘ └┘ └─────┘
src └───────────┘ └──────────┘ └─────┘
typ └───────────┘ └┘ └──────────┘ └┘ └┘ └─────┘
277 Union_nat := assume s, ennreal.le_of_forall_epsilon_le $ begin
id ┴ └─────────────────────────────┘
src └─────────────────────────────┘
typ ┴ └─────────────────────────────┘
st └─────
278 assume ε hε (hb : (∑i, μ (s i)) < ⊤),
id ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴┴┴┴ ┴ ┴ └─┘┴┴┴┴
typ └────────────────┘ ┴┴┴┴┴┴ ┴┴ └─┘┴┴┴┴
doc └────────────────┘ ┴┴┴┴ ┴ ┴ └─┘ ┴ ┴
txt └────────────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
par └────────────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
pid └────────────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
st ───────────────────────────────────────┘└─
279 rcases ennreal.exists_pos_sum_of_encodable (ennreal.coe_lt_coe.2 hε) ℕ with ⟨ε', hε', hl⟩,
id └─────────────────────────────────┘ └────────────────┘ └┘
src └─────┘└─────────────────────────────────┘┴ └────────────────┘└─┘ └┘ └─────────────────┘
typ └─────┘└─────────────────────────────────┘┴ └────────────────┘└─┘└┘└┘ └─────────────────┘
doc └─────┘ ┴ └─┘ └┘ └─────────────────┘
txt └─────┘ ┴ └─┘ └┘ └─────────────────┘
par └─────┘ ┴ └─┘ └┘ └─────────────────┘
pid ┴ ┴ └─┘ └┘ └─────────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
280 refine le_trans _ (add_le_add_left' (le_of_lt hl)),
id └──────┘ └──────────────┘ └──────┘ └┘
src └─────┘└──────┘└─┘ └──────────────┘┴ └──────┘┴ └┘
typ └─────┘└──────┘└─┘ └──────────────┘┴ └──────┘┴└┘└┘
doc └─────┘ └─┘ ┴ ┴ └┘
txt └─────┘ └─┘ ┴ ┴ └┘
par └─────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ └┘
st ─────────────────────────────────────────────────────┘└─
281 rw ← ennreal.tsum_add,
id └──────────────┘
src └───┘└──────────────┘
typ └───┘└──────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────────────────────┘└─
282 choose f hf using show
src └────────────────┘ └
typ └────────────────┘ └
doc └────────────────┘ └
txt └────────────────┘ └
par └────────────────┘ └
pid └┘└─┘└─────┘ └
st ───────────────────────────
283 ∀i, ∃f:ℕ → set α, s i ⊆ (⋃i, f i) ∧ (∑i, m (f i)) < μ (s i) + ε' i,
id ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src ─────┘ ┴ ┴┴└┘ ┴ ┴└─┘┴ ┴┴ ┴ ┴┴┴ ┴┴┴┴ ┴ └┘ ┴ ┴┴┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘┴┴ ┴ └─
typ ─────┘ ┴ ┴┴└┘ ┴┴┴└─┘┴┴┴┴ ┴ ┴┴┴ ┴┴┴┴ ┴ └┘ ┴ ┴┴┴┴┴┴ ┴ └─┘ ┴┴┴ ┴┴ └┘┴┴└┘┴ └─
doc ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴ ┴ └┘ ┴ ┴┴┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─
txt ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─
par ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─
pid ─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────────────
284 { intro,
src ─────┘└───┘└─
typ ─────┘└───┘└─
doc ─────┘└───┘└─
txt ─────┘└───┘└─
par ─────┘└───┘└─
pid ─────────────
st ────┘└────┘└─
285 have : μ (s i) < μ (s i) + ε' i :=
id ┴ ┴ └┘ ┴
src ─────┘└─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───
typ ─────┘└─────┘ ┴ ┴ └┘ ┴┴┴ ┴┴ └┘ ┴└┘┴┴└───
doc ─────┘└─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───
txt ─────┘└─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───
par ─────┘└─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───
pid ────────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───
st ─────────────────────────────────────────
286 ennreal.lt_add_right
id └──────────────────┘
src ───────┘└──────────────────┘└
typ ───────┘└──────────────────┘└
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ─────────────────────────────
287 (lt_of_le_of_lt (by apply ennreal.le_tsum) hb)
id └────────────┘ └─────────────┘ └┘
src ─────────┘ └────────────┘┴ ┴└────┘└─────────────┘└┘ └─
typ ─────────┘ └────────────┘┴ ┴└────┘└─────────────┘└┘└┘└─
doc ─────────┘ ┴ ┴└────┘ └┘ └─
txt ─────────┘ ┴ ┴└────┘ └┘ └─
par ─────────┘ ┴ ┴└────┘ └┘ └─
pid ─────────┘ ┴ └─────┘ └┘ └─
st ────────────────────────────┘└────────────────────┘└─────
288 (by simpa using hε' i),
id └─┘ ┴
src ─────────┘ ┴└──────────┘ ┴ ┴└─
typ ─────────┘ ┴└──────────┘└─┘┴┴┴└─
doc ─────────┘ ┴└──────────┘ ┴ ┴└─
txt ─────────┘ ┴└──────────┘ ┴ ┴└─
par ─────────┘ ┴└──────────┘ ┴ ┴└─
pid ─────────┘ └───────────┘ ┴ └──
st ────────────┘└────────────────┘┴└─
289 simpa [μ, infi_lt_iff] },
id ┴ └─────────┘
src ─────┘└─────┘ └┘└─────────┘└┘┴
typ ─────┘└─────┘┴└┘└─────────┘└┘┴
doc ─────┘└─────┘ └┘ └┘┴
txt ─────┘└─────┘ └┘ └┘┴
par ─────┘└─────┘ └┘ └┘┴
pid ────────────┘ └┘ └─┘
st ────────────────────────────┘└┘└
290 refine le_trans _ (ennreal.tsum_le_tsum $ λ i, le_of_lt (hf i).2),
id └──────┘ └──────────────────┘ └──────┘ └┘
src └─────┘└──────┘└─┘ └──────────────────┘┴ ┴ └──┘└──────┘┴ ┴ └──┘
typ └─────┘└──────┘└─┘ └──────────────────┘┴ ┴ └──┘└──────┘┴ └┘┴ └──┘
doc └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
txt └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
par └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
pid ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
st ────────────────────────────────────────────────────────────────────┘└─
291 rw [← ennreal.tsum_prod, ← tsum_equiv equiv.nat_prod_nat_equiv_nat.symm],
id └───────────────┘ └────────┘ └───────────────────────────────┘
src └────┘└───────────────┘└──┘└────────┘┴└───────────────────────────────┘┴
typ └────┘└───────────────┘└──┘└────────┘┴└───────────────────────────────┘┴
doc └────┘ └──┘ ┴ ┴
txt └────┘ └──┘ ┴ ┴
par └────┘ └──┘ ┴ ┴
pid └──┘ └──┘ ┴ ┴
st ──────────────────────────┘└──────────────────────────────────────────────┘└──
292 swap, {apply_instance},
src └──┘ └────────────┘
typ └──┘ └────────────┘
doc └──┘ └────────────┘
txt └──┘ └────────────┘
par └──┘ └────────────┘
st ───────┘└───────────────┘└┘└
293 refine infi_le_of_le _ (infi_le _ _),
id └───────────┘ └─────┘
src └─────┘└───────────┘└─┘ └─────┘└───┘
typ └─────┘└───────────┘└─┘ └─────┘└───┘
doc └─────┘ └─┘ └───┘
txt └─────┘ └─┘ └───┘
par └─────┘ └─┘ └───┘
pid ┴ └─┘ └───┘
st ───────────────────────────────────────┘└─
294 exact Union_subset (λ i, subset.trans (hf i).1 $
id └┘
src └────┘ ┴ └──┘ ┴ ┴ └──┘ └
typ └────┘ ┴ └──┘ ┴ └┘┴ └──┘ └
doc └────┘ ┴ └──┘ ┴ ┴ └──┘ └
txt └────┘ ┴ └──┘ ┴ ┴ └──┘ └
par └────┘ ┴ └──┘ ┴ ┴ └──┘ └
pid ┴ ┴ └──┘ ┴ ┴ └──┘ └
st ─────────────────────────────────────────────────────
295 Union_subset $ λ j, subset.trans (by simp) $
id └──────────┘ └──────────┘
src ─────┘└──────────┘┴ ┴ └──┘└──────────┘┴ ┴└──┘└┘ └
typ ─────┘└──────────┘┴ ┴ └──┘└──────────┘┴ ┴└──┘└┘ └
doc ─────┘ ┴ ┴ └──┘ ┴ ┴└──┘└┘ └
txt ─────┘ ┴ ┴ └──┘ ┴ ┴└──┘└┘ └
par ─────┘ ┴ ┴ └──┘ ┴ ┴└──┘└┘ └
pid ─────┘ ┴ ┴ └──┘ ┴ └─────┘ └
st ─────────────────────────────────────────┘└───┘└───
296 subset_Union _ $ equiv.nat_prod_nat_equiv_nat (i, j)),
id └──────────┘ └──────────────────────────┘
src ─────┘└──────────┘└─┘ ┴└──────────────────────────┘┴ └┘ └┘
typ ─────┘└──────────┘└─┘ ┴└──────────────────────────┘┴ └┘ └┘
doc ─────┘ └─┘ ┴ ┴ └┘ └┘
txt ─────┘ └─┘ ┴ ┴ └┘ └┘
par ─────┘ └─┘ ┴ ┴ └┘ └┘
pid ─────┘ └─┘ ┴ ┴ └┘ └┘
st ──────────────────────────────────────────────────────────┘└─
297 end }
st ────┘
298
299 theorem of_function_le {α : Type*} (m : set α → ennreal) (m_empty s) :
id └─┘ ┴ └─────┘
src └─┘ └─────┘
typ └─┘ ┴ └─────┘
doc └─────┘
300 outer_measure.of_function m m_empty s ≤ m s :=
id └───────────────────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src └───────────────────────┘ ┴
typ └───────────────────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └───────────────────────┘
301 let f : ℕ → set α := λi, nat.rec_on i s (λn s, ∅) in
id ┴ ┴ └─┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ └────────┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
302 infi_le_of_le f $ infi_le_of_le (subset_Union f 0) $ le_of_eq $
id └───────────┘ ┴ └───────────┘ └──────────┘ ┴ └──────┘
src └───────────┘ └───────────┘ └──────────┘ └──────┘
typ └───────────┘ ┴ └───────────┘ └──────────┘ ┴ └──────┘
303 calc (∑i, m (f i)) = ({0} : finset ℕ).sum (λi, m (f i)) :
id ┴┴┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └────┘ ┴ └─┘
typ ┴┴┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc ┴ ┴ └────┘
304 tsum_eq_sum $ by intro i; cases i; simp [m_empty]
id └─────────┘ ┴ └─────┘
src └─────────┘ └─────┘ └────┘ └────┘ └─
typ └─────────┘ └─────┘ └────┘┴ └────┘└─────┘└─
doc └─────┘ └────┘ └────┘ └─
txt └─────┘ └────┘ └────┘ └─
par └─────┘ └────┘ └────┘ └─
pid └┘ ┴ ┴┴ ┴└
st └─────────────────────────────────
305 ... = m s : by simp; refl
id ┴ ┴
src ─┘ └──┘ └────
typ ─┘ ┴ ┴ └──┘ └────
doc ─┘ └──┘ └────
txt ─┘ └──┘ └────
par ─┘ └──┘ └────
pid ─┘ └
st ─┘ └───────────
306
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
307 theorem le_of_function {α : Type*} {m m_empty} {μ : outer_measure α} :
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
308 μ ≤ outer_measure.of_function m m_empty ↔ ∀ s, μ s ≤ m s :=
id ┴ ┴ └───────────────────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────────────────────┘ ┴ ┴
typ ┴ ┴ └───────────────────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────────────┘
309 ⟨λ H s, le_trans (H _) (of_function_le _ _ _),
id ┴ ┴ └──────┘ ┴ └────────────┘
src └──────┘ └────────────┘
typ ┴ ┴ └──────┘ ┴ └────────────┘
310 λ H s, le_infi $ λ f, le_infi $ λ hs,
id ┴ ┴ └─────┘ ┴ └─────┘ └┘
src └─────┘ └─────┘
typ ┴ ┴ └─────┘ ┴ └─────┘ └┘
311 le_trans (μ.mono hs) $ le_trans (μ.Union f) $
id └──────┘ ┴└───┘ └┘ └──────┘ ┴└────┘ ┴
src └──────┘ └───┘ └──────┘ └────┘
typ └──────┘ ┴└───┘ └┘ └──────┘ ┴└────┘ ┴
312 ennreal.tsum_le_tsum $ λ i, H _⟩
id └──────────────────┘ ┴ ┴
src └──────────────────┘
typ └──────────────────┘ ┴ ┴
313
314 end of_function
315
316 section caratheodory_measurable
317 universe u
318 parameters {α : Type u} (m : outer_measure α)
id ┴ └───────────┘
src └───────────┘
typ ┴ └───────────┘
319 include m
320
321 local attribute [simp] set.inter_comm set.inter_left_comm set.inter_assoc
id └────────────┘ └─────────────────┘ └─────────────┘
src └────────────┘ └─────────────────┘ └─────────────┘
typ └────────────┘ └─────────────────┘ └─────────────┘
doc └──┘
322
323 variables {s s₁ s₂ : set α}
id └─┘
src └─┘
typ └─┘
324
325 private def C (s : set α) := ∀t, m t = m (t ∩ s) + m (t \ s)
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
326
327 private lemma C_iff_le {s : set α} : C s ↔ ∀t, m (t ∩ s) + m (t \ s) ≤ m t :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
328 forall_congr $ λ t, le_antisymm_iff.trans $ and_iff_right $
id └──────────┘ ┴ └─────────────┘└────┘ └───────────┘
src └──────────┘ └─────────────┘└────┘ └───────────┘
typ └──────────┘ ┴ └─────────────┘└────┘ └───────────┘
329 by convert m.union _ _; rw inter_union_diff t s
id └─────┘ └──────────────┘ ┴ ┴
src └──────┘└─────┘└──┘ └─┘└──────────────┘┴ ┴ └
typ └──────┘└─────┘└──┘ └─┘└──────────────┘┴┴┴┴└
doc └──────┘ └──┘ └─┘ ┴ ┴ └
txt └──────┘ └──┘ └─┘ ┴ ┴ └
par └──────┘ └──┘ └─┘ ┴ ┴ └
pid ┴ └──┘ ┴ ┴ ┴ └
st └───────────────────────┘└──────────────┘└────
330
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
331 @[simp] private lemma C_empty : C ∅ := by simp [C, m.empty, diff_empty]
id ┴ ┴ ┴ └────────┘
src ┴ ┴ └────┘┴└┘ └┘└────────┘└─
typ ┴ ┴ └────┘┴└┘└─────┘└┘└────────┘└─
doc └──┘ └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └──────────────────────────────
332
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
333 private lemma C_compl : C s₁ → C (- s₁) := by simp [C, diff_eq]
id ┴ └┘ ┴ ┴ └┘ ┴ └─────┘
src ┴ ┴ ┴ └────┘┴└┘└─────┘└─
typ ┴ └┘ ┴ ┴ └┘ └────┘┴└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────
334
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
335 @[simp] private lemma C_compl_iff : C (- s) ↔ C s :=
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
336 ⟨λ h, by simpa using C_compl m h, C_compl⟩
id ┴ └─────┘ ┴ ┴ └─────┘
src └──────────┘└─────┘┴ ┴ └─────┘
typ ┴ └──────────┘└─────┘┴┴┴┴ └─────┘
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid ┴└────┘ ┴ ┴
st └──────────────────────┘
337
338 private lemma C_union (h₁ : C s₁) (h₂ : C s₂) : C (s₁ ∪ s₂) :=
id ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
339 λ t, begin
id ┴
typ ┴
st └─────
340 rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)),
id └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘
src └──┘ ┴ └┘ ┴ ┴┴┴ └─┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴ ┴┴┴ └───
typ └──┘└┘┴┴└┘└┘┴ ┴┴┴┴└┘└─┘└┘┴ ┴┴┴┴└┘└─┘└┘┴ ┴┴ ┴ └┘┴┴┴└┘└───
doc └──┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───
txt └──┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───
par └──┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───
pid └┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └───
st ─────────┘└───────────┘└───────────┘└──────────────────┘└─
341 inter_diff_assoc _ _ s₁, set.inter_assoc _ _ s₁,
id └──────────────┘ └┘ └─────────────┘ └┘
src ───┘└──────────────┘└───┘ └┘└─────────────┘└───┘ └─
typ ───┘└──────────────┘└───┘└┘└┘└─────────────┘└───┘└┘└─
doc ───┘ └───┘ └┘ └───┘ └─
txt ───┘ └───┘ └┘ └───┘ └─
par ───┘ └───┘ └┘ └───┘ └─
pid ───┘ └───┘ └┘ └───┘ └─
st ──────────────────────────┘└──────────────────────┘└─
342 inter_eq_self_of_subset_right (set.subset_union_left _ _),
id └───────────────────────────┘ └───────────────────┘
src ───┘└───────────────────────────┘┴ └───────────────────┘└──────
typ ───┘└───────────────────────────┘┴ └───────────────────┘└──────
doc ───┘ ┴ └──────
txt ───┘ ┴ └──────
par ───┘ ┴ └──────
pid ───┘ ┴ └──────
st ────────────────────────────────────────────────────────────┘└─
343 union_diff_left, h₂ (t ∩ s₁)],
id └─────────────┘ └┘ ┴ └┘
src ───┘└─────────────┘└┘ ┴ ┴ ┴ └┘
typ ───┘└─────────────┘└┘└┘┴ ┴┴ ┴└┘└┘
doc ───┘ └┘ ┴ ┴ ┴ └┘
txt ───┘ └┘ ┴ ┴ ┴ └┘
par ───┘ └┘ ┴ ┴ ┴ └┘
pid ───┘ └┘ ┴ ┴ ┴ └┘
st ──────────────────┘└───────────┘└──
344 simp [diff_eq]
id └─────┘
src └────┘└─────┘└┘
typ └────┘└─────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ────────────────┘
345 end
st └─┘
346
347 private lemma measure_inter_union (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : C s₁) {t : set α} :
id └┘ ┴ └┘ ┴ ┴ ┴ └┘ └─┘ ┴
src ┴ ┴ ┴ ┴ └─┘
typ └┘ ┴ └┘ ┴ ┴ ┴ └┘ └─┘ ┴
348 m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂) :=
id ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
349 by rw [h₁, set.inter_assoc, set.union_inter_cancel_left,
id └┘ └─────────────┘ └─────────────────────────┘
src └──┘ └┘└─────────────┘└┘└─────────────────────────┘└─
typ └──┘└┘└┘└─────────────┘└┘└─────────────────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ └─
st └─────┘└───────────────┘└───────────────────────────┘└─
350 inter_diff_assoc, union_diff_cancel_left h]
id └──────────────┘ └────────────────────┘ ┴
src ─┘└──────────────┘└┘└────────────────────┘┴ └─
typ ─┘└──────────────┘└┘└────────────────────┘┴┴└─
doc ─┘ └┘ ┴ └─
txt ─┘ └┘ ┴ └─
par ─┘ └┘ ┴ └─
pid ─┘ └┘ ┴ ┴└
st ─────────────────┘└────────────────────────┘┴└
351
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
352 private lemma C_Union_lt {s : ℕ → set α} : ∀{n:ℕ}, (∀i<n, C (s i)) → C (⋃i<n, s i)
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc ┴ ┴
353 | 0 h := by simp [nat.not_lt_zero]
id └─────────────┘
src └────┘└─────────────┘└┘
typ └────┘└─────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └──────────────────────┘
354 | (n + 1) h := by rw Union_lt_succ; exact C_union m
id ┴ └───────────┘ └─────┘ ┴
src ┴ └─┘└───────────┘ └────┘└─────┘┴ └
typ ┴ └─┘└───────────┘ └────┘└─────┘┴┴└
doc └─┘ └────┘ ┴ └
txt └─┘ └────┘ ┴ └
par └─┘ └────┘ ┴ └
pid ┴ ┴ ┴ └
st └──────────────────────────────────
355 (h n (le_refl (n + 1)))
id └─────┘ ┴ ┴
src ─┘ ┴ ┴ └─────┘┴ ┴┴└─────
typ ─┘ ┴ ┴ └─────┘┴ ┴┴┴└─────
doc ─┘ ┴ ┴ ┴ ┴ └─────
txt ─┘ ┴ ┴ ┴ ┴ └─────
par ─┘ ┴ ┴ ┴ ┴ └─────
pid ─┘ ┴ ┴ ┴ ┴ └─────
st ──────────────────────────
356 (C_Union_lt $ assume i hi, h i $ lt_of_lt_of_le hi $ nat.le_succ _)
id └────────┘ ┴ └────────────┘ └─────────┘
src ─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴└────────────┘┴ ┴ ┴└─────────┘└───
typ ─────┘ └────────┘┴ ┴ └─────┘┴┴ ┴ ┴└────────────┘┴ ┴ ┴└─────────┘└───
doc ─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
txt ─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
par ─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid ─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└
st ──────────────────────────────────────────────────────────────────────────
357
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
358 private lemma C_inter (h₁ : C s₁) (h₂ : C s₂) : C (s₁ ∩ s₂) :=
id ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘
359 by rw [← C_compl_iff, compl_inter]; from C_union _ (C_compl _ h₁) (C_compl _ h₂)
id └─────────┘ └─────────┘ └─────┘ └┘ └─────┘ └┘
src └────┘└─────────┘└┘└─────────┘┴ └───┘└─────┘└─┘ └─┘ └┘ └─────┘└─┘ └─
typ └────┘└─────────┘└┘└─────────┘┴ └───┘└─────┘└─┘ └─┘└┘└┘ └─────┘└─┘└┘└─
doc └────┘ └┘ ┴ └───┘ └─┘ └─┘ └┘ └─┘ └─
txt └────┘ └┘ ┴ └───┘ └─┘ └─┘ └┘ └─┘ └─
par └────┘ └┘ ┴ └───┘ └─┘ └─┘ └┘ └─┘ └─
pid └──┘ └┘ ┴ └───┘ └─┘ └─┘ └┘ └─┘ ┴└
st └────────────────┘└───────────┘┴└──────────────────────────────────────────────
360
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
361 private lemma C_sum {s : ℕ → set α} (h : ∀i, C (s i)) (hd : pairwise (disjoint on s)) {t : set α} :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └──────┘ └┘ ┴ └─┘ ┴
src ┴ └─┘ ┴ └──────┘ └──────┘ └┘ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └──────┘ └┘ ┴ └─┘ ┴
doc └──────┘ └──────┘
362 ∀ {n}, (finset.range n).sum (λi, m (t ∩ s i)) = m (t ∩ ⋃i<n, s i)
id ┴┴ └──────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src └──────────┘ └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴┴ └──────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └──────────┘ ┴ ┴
363 | 0 := by simp [nat.not_lt_zero, m.empty]
id └─────────────┘
src └────┘└─────────────┘└┘ └┘
typ └────┘└─────────────┘└┘└─────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └───────────────────────────────┘
364 | (nat.succ n) := begin
id └──────┘
src └──────┘
typ └──────┘
st └─────
365 simp [Union_lt_succ, range_succ],
id └───────────┘ └────────┘
src └────┘└───────────┘└┘└────────┘┴
typ └────┘└───────────┘└┘└────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ─────────────────────────────────┘└─
366 rw [measure_inter_union m _ (h n), C_sum],
id └─────────────────┘ ┴ ┴ ┴
src └──┘└─────────────────┘┴ └─┘ ┴ └─┘ ┴
typ └──┘└─────────────────┘┴┴└─┘ ┴┴┴└─┘└───┘┴
doc └──┘ ┴ └─┘ ┴ └─┘ ┴
txt └──┘ ┴ └─┘ ┴ └─┘ ┴
par └──┘ ┴ └─┘ ┴ └─┘ ┴
pid └┘ ┴ └─┘ ┴ └─┘ ┴
st ──────────────────────────────────┘└─────┘└──
367 intro a, simpa [range_succ] using λ h₁ i hi h₂, hd _ _ (ne_of_gt hi) ⟨h₁, h₂⟩
id └────────┘ └┘ └──────┘
src └─────┘ └─────┘└────────┘└──────┘ └───────────┘ └───┘ └──────┘┴ └┘ └┘ └┘
typ └─────┘ └─────┘└────────┘└──────┘ └───────────┘└┘└───┘ └──────┘┴ └┘ └┘ └┘
doc └─────┘ └─────┘ └──────┘ └───────────┘ └───┘ ┴ └┘ └┘ └┘
txt └─────┘ └─────┘ └──────┘ └───────────┘ └───┘ ┴ └┘ └┘ └┘
par └─────┘ └─────┘ └──────┘ └───────────┘ └───┘ ┴ └┘ └┘ └┘
pid └┘ ┴┴ ┴┴└────┘ └───────────┘ └───┘ ┴ └┘ └┘ ┴┴
st ────────┘└─────────────────────────────────────────────────────────────────────┘
368 end
st └─┘
369
370 private lemma C_Union_nat {s : ℕ → set α} (h : ∀i, C (s i))
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
371 (hd : pairwise (disjoint on s)) : C (⋃i, s i) :=
id └──────┘ └──────┘ └┘ ┴ ┴ ┴┴┴ ┴ ┴
src └──────┘ └──────┘ └┘ ┴ ┴ ┴
typ └──────┘ └──────┘ └┘ ┴ ┴ ┴┴┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴
372 C_iff_le.2 $ λ t, begin
id └──────┘┴ ┴
src └──────┘┴
typ └──────┘┴ ┴
st └─────
373 have hp : m (t ∩ ⋃i, s i) ≤ (⨆n, m (t ∩ ⋃i<n, s i)),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴┴┴ ┴ ┴ ┴ └┘┴┴ ┴┴┴┴ ┴ ┴ ┴┴└┘ ┴┴ ┴ └┘
typ └────────┘ ┴ ┴┴┴ ┴ ┴ ┴ └┘┴┴ ┴┴┴┴┴┴ ┴┴ ┴┴└┘ ┴┴┴┴ └┘
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴┴┴ ┴ ┴ ┴┴└┘ ┴┴ ┴ └┘
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
st ────────────────────────────────────────────────────┘└─
374 { convert m.Union (λ i, t ∩ s i),
id └─────┘ ┴ ┴
src └──────┘└─────┘┴ └──┘ ┴ ┴ ┴ ┴
typ └──────┘└─────┘┴ └──┘┴┴ ┴┴┴ ┴
doc └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴
txt └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴
par └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴
pid ┴ ┴ └──┘ ┴ ┴ ┴ ┴
st ───┘└────────────────────────────┘└─
375 { rw inter_Union },
id └─────────┘
src └─┘└─────────┘┴
typ └─┘└─────────┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────┘└─────────────┘└┘└
376 { simp [ennreal.tsum_eq_supr_nat, C_sum m h hd] } },
id └──────────────────────┘ └───┘ ┴ ┴ └┘
src └────┘└──────────────────────┘└┘└───┘┴ ┴ ┴ └┘
typ └────┘└──────────────────────┘└┘└───┘┴┴┴┴┴└┘└┘
doc └────┘ └┘ ┴ ┴ ┴ └┘
txt └────┘ └┘ ┴ ┴ ┴ └┘
par └────┘ └┘ ┴ ┴ ┴ └┘
pid ┴┴ └┘ ┴ ┴ ┴ ┴┴
st ───────────────────────────────────────────────────┘└──┘└
377 refine le_trans (add_le_add_right' hp) _,
id └──────┘ └───────────────┘ └┘
src └─────┘└──────┘┴ └───────────────┘┴ └─┘
typ └─────┘└──────┘┴ └───────────────┘┴└┘└─┘
doc └─────┘ ┴ ┴ └─┘
txt └─────┘ ┴ ┴ └─┘
par └─────┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────┘└─
378 rw ennreal.supr_add,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
379 refine supr_le (λ n, le_trans (add_le_add_left' _)
id └─────┘ └──────┘ └──────────────┘
src └─────┘└─────┘┴ └──┘└──────┘┴ └──────────────┘└───
typ └─────┘└─────┘┴ └──┘└──────┘┴ └──────────────┘└───
doc └─────┘ ┴ └──┘ ┴ └───
txt └─────┘ ┴ └──┘ ┴ └───
par └─────┘ ┴ └──┘ ┴ └───
pid ┴ ┴ └──┘ ┴ └───
st ─────────────────────────────────────────────────────
380 (ge_of_eq (C_Union_lt m (λ i _, h i) _))),
id └──────┘ └────────┘ ┴ ┴
src ───┘ └──────┘┴ └────────┘┴ ┴ └────┘ ┴ └────┘
typ ───┘ └──────┘┴ └────────┘┴┴┴ └────┘┴┴ └────┘
doc ───┘ ┴ ┴ ┴ └────┘ ┴ └────┘
txt ───┘ ┴ ┴ ┴ └────┘ ┴ └────┘
par ───┘ ┴ ┴ ┴ └────┘ ┴ └────┘
pid ───┘ ┴ ┴ ┴ └────┘ ┴ └────┘
st ────────────────────────────────────────────┘└─
381 refine m.mono (diff_subset_diff_right _),
id └────┘ └────────────────────┘
src └─────┘└────┘┴ └────────────────────┘└─┘
typ └─────┘└────┘┴ └────────────────────┘└─┘
doc └─────┘ ┴ └─┘
txt └─────┘ ┴ └─┘
par └─────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ─────────────────────────────────────────┘└─
382 exact bUnion_subset (λ i _, subset_Union _ i),
id └───────────┘ └──────────┘
src └────┘└───────────┘┴ └────┘└──────────┘└─┘ ┴
typ └────┘└───────────┘┴ └────┘└──────────┘└─┘ ┴
doc └────┘ ┴ └────┘ └─┘ ┴
txt └────┘ ┴ └────┘ └─┘ ┴
par └────┘ ┴ └────┘ └─┘ ┴
pid ┴ ┴ └────┘ └─┘ ┴
st ──────────────────────────────────────────────┘└─
383 end
st ──┘
384
385 private lemma f_Union {s : ℕ → set α} (h : ∀i, C (s i))
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
386 (hd : pairwise (disjoint on s)) : m (⋃i, s i) = ∑i, m (s i) :=
id └──────┘ └──────┘ └┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src └──────┘ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴
typ └──────┘ └──────┘ └┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc └──────┘ └──────┘ ┴ ┴ ┴ ┴
387 begin
st └─────
388 refine le_antisymm (m.Union_nat s) _,
id └─────────┘ └─────────┘ ┴
src └─────┘└─────────┘┴ └─────────┘┴ └─┘
typ └─────┘└─────────┘┴ └─────────┘┴┴└─┘
doc └─────┘ ┴ ┴ └─┘
txt └─────┘ ┴ ┴ └─┘
par └─────┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ └─┘
st ─────────────────────────────────────┘└─
389 rw ennreal.tsum_eq_supr_nat,
id └──────────────────────┘
src └─┘└──────────────────────┘
typ └─┘└──────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────────────┘└─
390 refine supr_le (λ n, _),
id └─────┘
src └─────┘└─────┘┴ └────┘
typ └─────┘└─────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ────────────────────────┘└─
391 have := @C_sum _ m _ h hd univ n,
id └───┘ ┴ ┴ └┘ └──┘ ┴
src └──────┘ └───┘└─┘ └─┘ ┴ ┴└──┘┴
typ └──────┘ └───┘└─┘┴└─┘┴┴└┘┴└──┘┴┴
doc └──────┘ └─┘ └─┘ ┴ ┴ ┴
txt └──────┘ └─┘ └─┘ ┴ ┴ ┴
par └──────┘ └─┘ └─┘ ┴ ┴ ┴
pid └───┘└─┘ └─┘ └─┘ ┴ ┴ ┴
st ─────────────────────────────────┘└─
392 simp at this, simp [this],
id └──┘
src └──────────┘ └────┘ ┴
typ └──────────┘ └────┘└──┘┴
doc └──────────┘ └────┘ ┴
txt └──────────┘ └────┘ ┴
par └──────────┘ └────┘ ┴
pid ┴└─────┘ ┴┴ ┴
st ─────────────┘└───────────┘└─
393 exact m.mono (bUnion_subset (λ i _, subset_Union _ i)),
id └────┘ └───────────┘ └──────────┘
src └────┘└────┘┴ └───────────┘┴ └────┘└──────────┘└─┘ └┘
typ └────┘└────┘┴ └───────────┘┴ └────┘└──────────┘└─┘ └┘
doc └────┘ ┴ ┴ └────┘ └─┘ └┘
txt └────┘ ┴ ┴ └────┘ └─┘ └┘
par └────┘ ┴ ┴ └────┘ └─┘ └┘
pid ┴ ┴ ┴ └────┘ └─┘ └┘
st ───────────────────────────────────────────────────────┘└─
394 end
st ──┘
395
396 private def caratheodory_dynkin : measurable_space.dynkin_system α :=
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
397 { has := C,
id ┴
src ┴
typ ┴
398 has_empty := C_empty,
id └─────┘
src └─────┘
typ └─────┘
399 has_compl := assume s, C_compl,
id ┴ └─────┘
src └─────┘
typ ┴ └─────┘
400 has_Union_nat := assume f hf hn, C_Union_nat hn hf }
id ┴ └┘ └┘ └─────────┘ └┘ └┘
src └─────────┘
typ ┴ └┘ └┘ └─────────┘ └┘ └┘
401
402 /-- Given an outer measure `μ`, the Caratheodory measurable space is
403 defined such that `s` is measurable if `∀t, μ t = μ (t ∩ s) + μ (t \ s)`. -/
404 protected def caratheodory : measurable_space α :=
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
405 caratheodory_dynkin.to_measurable_space $ assume s₁ s₂, C_inter
id └─────────────────┘└──────────────────┘ └┘ └┘ └─────┘
src └─────────────────┘└──────────────────┘ └─────┘
typ └─────────────────┘└──────────────────┘ └┘ └┘ └─────┘
406
407 lemma is_caratheodory {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
408 caratheodory.is_measurable s ↔ ∀t, m t = m (t ∩ s) + m (t \ s) :=
id └──────────┘└────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘└────────────┘ ┴ ┴ ┴ ┴ ┴
typ └──────────┘└────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
409 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
410
411 lemma is_caratheodory_le {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
412 caratheodory.is_measurable s ↔ ∀t, m (t ∩ s) + m (t \ s) ≤ m t :=
id └──────────┘└────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘└────────────┘ ┴ ┴ ┴ ┴ ┴
typ └──────────┘└────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
413 C_iff_le
id └──────┘
src └──────┘
typ └──────┘
414
415 protected lemma Union_eq_of_caratheodory {s : ℕ → set α}
id ┴ └─┘ ┴
src ┴ └─┘
typ ┴ └─┘ ┴
416 (h : ∀i, caratheodory.is_measurable (s i)) (hd : pairwise (disjoint on s)) :
id ┴ └──────────┘└────────────┘ ┴ ┴ └──────┘ └──────┘ └┘ ┴
src └──────────┘└────────────┘ └──────┘ └──────┘ └┘
typ ┴ └──────────┘└────────────┘ ┴ ┴ └──────┘ └──────┘ └┘ ┴
doc └──────────┘ └──────┘ └──────┘
417 m (⋃i, s i) = ∑i, m (s i) :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
418 f_Union h hd
id └─────┘ ┴ └┘
src └─────┘
typ └─────┘ ┴ └┘
419
420 end caratheodory_measurable
421
422 variables {α : Type*}
423
424 lemma caratheodory_is_measurable {m : set α → ennreal} {s : set α}
id └─┘ ┴ └─────┘ └─┘ ┴
src └─┘ └─────┘ └─┘
typ └─┘ ┴ └─────┘ └─┘ ┴
doc └─────┘
425 {h₀ : m ∅ = 0} (hs : ∀t, m (t ∩ s) + m (t \ s) ≤ m t) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
426 (outer_measure.of_function m h₀).caratheodory.is_measurable s :=
id └───────────────────────┘ ┴ └┘ └──────────┘ └───────────┘ ┴
src └───────────────────────┘ └──────────┘ └───────────┘
typ └───────────────────────┘ ┴ └┘ └──────────┘ └───────────┘ ┴
doc └───────────────────────┘ └──────────┘
427 let o := (outer_measure.of_function m h₀) in
id ┴ └───────────────────────┘ ┴ └┘
src └───────────────────────┘
typ ┴ └───────────────────────┘ ┴ └┘
doc └───────────────────────┘
428 (is_caratheodory_le o).2 $ λ t,
id └────────────────┘ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴
429 le_infi $ λ f, le_infi $ λ hf, begin
id └─────┘ ┴ └─────┘ └┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ └┘
st └─────
430 refine le_trans (add_le_add'
id └──────┘ └─────────┘
src └─────┘└──────┘┴ └─────────┘└
typ └─────┘└──────┘┴ └─────────┘└
doc └─────┘ ┴ └
txt └─────┘ ┴ └
par └─────┘ ┴ └
pid ┴ ┴ └
st ───────────────────────────────
431 (infi_le_of_le (λi, f i ∩ s) $ infi_le _ _)
id ┴
src ───┘ ┴ └─┘ ┴ ┴┴┴ └┘ ┴ └─────
typ ───┘ ┴ └─┘ ┴ ┴┴┴ └┘ ┴ └─────
doc ───┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─────
txt ───┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─────
par ───┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─────
pid ───┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─────
st ────────────────────────────────────────────────
432 (infi_le_of_le (λi, f i \ s) $ infi_le _ _)) _,
id └───────────┘ ┴ ┴ ┴ └─────┘
src ───┘ └───────────┘┴ └─┘ ┴ ┴┴┴ └┘ ┴└─────┘└──────┘
typ ───┘ └───────────┘┴ └─┘┴┴ ┴┴┴┴└┘ ┴└─────┘└──────┘
doc ───┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └──────┘
txt ───┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └──────┘
par ───┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └──────┘
pid ───┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └──────┘
st ─────────────────────────────────────────────────┘└─
433 { rw ← Union_inter,
id └─────────┘
src └───┘└─────────┘
typ └───┘└─────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ───┘└──────────────┘└─
434 exact inter_subset_inter_left _ hf },
id └─────────────────────┘ └┘
src └────┘└─────────────────────┘└─┘ ┴
typ └────┘└─────────────────────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────────────────────────┘└┘└
435 { rw ← Union_diff,
id └────────┘
src └───┘└────────┘
typ └───┘└────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ───┘└─────────────┘└─
436 exact diff_subset_diff_left hf },
id └───────────────────┘ └┘
src └────┘└───────────────────┘┴ ┴
typ └────┘└───────────────────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────┘└┘└
437 { rw ← ennreal.tsum_add,
id └──────────────┘
src └───┘└──────────────┘
typ └───┘└──────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────────────────────┘└─
438 exact ennreal.tsum_le_tsum (λ i, hs _) }
id └──────────────────┘ └┘
src └────┘└──────────────────┘┴ └──┘ └──┘
typ └────┘└──────────────────┘┴ └──┘└┘└──┘
doc └────┘ ┴ └──┘ └──┘
txt └────┘ ┴ └──┘ └──┘
par └────┘ ┴ └──┘ └──┘
pid ┴ ┴ └──┘ └─┘┴
st ──────────────────────────────────────────┘└─
439 end
st ──┘
440
441 @[simp] theorem zero_caratheodory : (0 : outer_measure α).caratheodory = ⊤ :=
id └───────────┘ ┴ └──────────┘ ┴ ┴
src └───────────┘ └──────────┘ ┴ ┴
typ └───────────┘ ┴ └──────────┘ ┴ ┴
doc └──┘ └──────────┘
442 top_unique $ λ s _ t, (add_zero _).symm
id └────────┘ ┴ ┴ ┴ └──────┘ └──┘
src └────────┘ └──────┘ └──┘
typ └────────┘ ┴ ┴ ┴ └──────┘ └──┘
443
444 theorem top_caratheodory : (⊤ : outer_measure α).caratheodory = ⊤ :=
id ┴ └───────────┘ ┴ └──────────┘ ┴ ┴
src ┴ └───────────┘ └──────────┘ ┴ ┴
typ ┴ └───────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘
445 top_unique $ assume s hs, (is_caratheodory_le _).2 $ assume t,
id └────────┘ ┴ └┘ └────────────────┘ ┴ ┴
src └────────┘ └────────────────┘ ┴
typ └────────┘ ┴ └┘ └────────────────┘ ┴ ┴
446 t.eq_empty_or_nonempty.elim (λ ht, by simp [ht])
id ┴└───────────────────┘└───┘ └┘ └┘
src └───────────────────┘└───┘ └────┘ ┴
typ ┴└───────────────────┘└───┘ └┘ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └────────┘
447 (λ ht, by simp only [ht, top_apply, le_top])
id └┘ └┘ └───────┘ └────┘
src └─────────┘ └┘└───────┘└┘└────┘┴
typ └┘ └─────────┘└┘└┘└───────┘└┘└────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └────────────────────────────────┘
448
449 theorem le_add_caratheodory (m₁ m₂ : outer_measure α) :
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
450 m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂ : outer_measure α).caratheodory :=
id └┘└───────────┘ ┴ └┘└───────────┘ ┴ └┘ ┴ └┘ └───────────┘ ┴ └──────────┘
src └───────────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ └──────────┘
typ └┘└───────────┘ ┴ └┘└───────────┘ ┴ └┘ ┴ └┘ └───────────┘ ┴ └──────────┘
doc └───────────┘ └───────────┘ └──────────┘
451 λ s ⟨hs₁, hs₂⟩ t, by simp [hs₁ t, hs₂ t]
id ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
src └────┘ ┴ └┘ ┴ └─
typ ┴ ┴ ┴ └────┘└─┘┴┴└┘└─┘┴┴└─
doc └────┘ ┴ └┘ ┴ └─
txt └────┘ ┴ └┘ ┴ └─
par └────┘ ┴ └┘ ┴ └─
pid ┴┴ ┴ └┘ ┴ ┴└
st └────────────────────
452
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
453 theorem le_sum_caratheodory {ι} (m : ι → outer_measure α) :
id ┴ └───────────┘ ┴
src └───────────┘
typ ┴ └───────────┘ ┴
454 (⨅ i, (m i).caratheodory) ≤ (sum m).caratheodory :=
id ┴ ┴┴ ┴ ┴ └──────────┘ ┴ └─┘ ┴ └──────────┘
src ┴ ┴ └──────────┘ ┴ └─┘ └──────────┘
typ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ └─┘ ┴ └──────────┘
doc ┴ ┴ └──────────┘ └──────────┘
455 λ s h t, by simp [λ i,
id ┴ ┴ ┴
src └────┘ └───
typ ┴ ┴ ┴ └────┘ └───
doc └────┘ └───
txt └────┘ └───
par └────┘ └───
pid ┴┴ └───
st └───────────
456 measurable_space.is_measurable_infi.1 h i t, ennreal.tsum_add]
id └─────────────────────────────────┘ ┴ ┴ └──────────────┘
src ─┘└─────────────────────────────────┘└─┘ ┴ ┴ └┘└──────────────┘└─
typ ─┘└─────────────────────────────────┘└─┘┴┴ ┴┴└┘└──────────────┘└─
doc ─┘ └─┘ ┴ ┴ └┘ └─
txt ─┘ └─┘ ┴ ┴ └┘ └─
par ─┘ └─┘ ┴ ┴ └┘ └─
pid ─┘ └─┘ ┴ ┴ └┘ ┴└
st ─────────────────────────────────────────────────────────────────
457
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
458 theorem le_smul_caratheodory (a : ennreal) (m : outer_measure α) :
id └─────┘ └───────────┘ ┴
src └─────┘ └───────────┘
typ └─────┘ └───────────┘ ┴
doc └─────┘
459 m.caratheodory ≤ (a • m).caratheodory :=
id ┴└───────────┘ ┴ ┴ ┴ ┴ └──────────┘
src └───────────┘ ┴ ┴ └──────────┘
typ ┴└───────────┘ ┴ ┴ ┴ ┴ └──────────┘
doc └───────────┘ └──────────┘
460 λ s h t, by simp [h t, mul_add]
id ┴ ┴ ┴ ┴ ┴ └─────┘
src └────┘ ┴ └┘└─────┘└─
typ ┴ ┴ ┴ └────┘┴┴┴└┘└─────┘└─
doc └────┘ ┴ └┘ └─
txt └────┘ ┴ └┘ └─
par └────┘ ┴ └┘ └─
pid ┴┴ ┴ └┘ ┴└
st └────────────────────
461
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
462 @[simp] theorem dirac_caratheodory (a : α) : (dirac a).caratheodory = ⊤ :=
id ┴ └───┘ ┴ └──────────┘ ┴ ┴
src └───┘ └──────────┘ ┴ ┴
typ ┴ └───┘ ┴ └──────────┘ ┴ ┴
doc └──┘ └───┘ └──────────┘
463 top_unique $ λ s _ t, begin
id └────────┘ ┴ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴ ┴
st └─────
464 by_cases a ∈ t; simp [h],
id ┴ ┴ ┴ ┴
src └───────┘ ┴┴┴ └────┘ ┴
typ └───────┘┴┴┴┴┴ └────┘┴┴
doc └───────┘ ┴ ┴ └────┘ ┴
txt └───────┘ ┴ ┴ └────┘ ┴
par └───────┘ ┴ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴┴ ┴
st ─────────────────────────┘└─
465 by_cases a ∈ s; simp [h]
id ┴ ┴ ┴
src └───────┘ ┴ ┴ └────┘ └┘
typ └───────┘┴┴ ┴┴ └────┘┴└┘
doc └───────┘ ┴ ┴ └────┘ └┘
txt └───────┘ ┴ ┴ └────┘ └┘
par └───────┘ ┴ ┴ └────┘ └┘
pid ┴ ┴ ┴ ┴┴ ┴┴
st ──────────────────────────┘
466 end
st └─┘
467
468 section Inf_gen
469
470 def Inf_gen (m : set (outer_measure α)) (s : set α) : ennreal :=
id └─┘ └───────────┘ ┴ └─┘ ┴ └─────┘
src └─┘ └───────────┘ └─┘ └─────┘
typ └─┘ └───────────┘ ┴ └─┘ ┴ └─────┘
doc └─────┘
471 ⨆(h : s.nonempty), ⨅ (μ : outer_measure α) (h : μ ∈ m), μ s
id ┴ ┴└───────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴ └───────────┘ ┴ ┴
typ ┴ ┴└───────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ └───────┘ ┴ ┴ ┴
472
473 @[simp] lemma Inf_gen_empty (m : set (outer_measure α)) : Inf_gen m ∅ = 0 :=
id └─┘ └───────────┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └───────────┘ └─────┘ ┴ ┴
typ └─┘ └───────────┘ ┴ └─────┘ ┴ ┴ ┴
doc └──┘
474 by simp [Inf_gen, empty_not_nonempty]
id └─────┘ └────────────────┘
src └────┘└─────┘└┘└────────────────┘└─
typ └────┘└─────┘└┘└────────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────────────────
475
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
476 lemma Inf_gen_nonempty1 (m : set (outer_measure α)) (t : set α) (h : t.nonempty) :
id └─┘ └───────────┘ ┴ └─┘ ┴ ┴└───────┘
src └─┘ └───────────┘ └─┘ └───────┘
typ └─┘ └───────────┘ ┴ └─┘ ┴ ┴└───────┘
doc └───────┘
477 Inf_gen m t = (⨅ (μ : outer_measure α) (h : μ ∈ m), μ t) :=
id └─────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └───────────┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
478 by rw [Inf_gen, supr_pos h]
id └─────┘ └──────┘ ┴
src └──┘└─────┘└┘└──────┘┴ └─
typ └──┘└─────┘└┘└──────┘┴┴└─
doc └──┘ └┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └──────────┘└──────────┘┴└
479
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
480 lemma Inf_gen_nonempty2 (m : set (outer_measure α)) (μ) (h : μ ∈ m) (t) :
id └─┘ └───────────┘ ┴ ┴ ┴ ┴
src └─┘ └───────────┘ ┴
typ └─┘ └───────────┘ ┴ ┴ ┴ ┴
481 Inf_gen m t = (⨅ (μ : outer_measure α) (h : μ ∈ m), μ t) :=
id └─────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └───────────┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
482 begin
st └─────
483 cases t.eq_empty_or_nonempty with ht ht,
id └────────────────────┘
src └────┘└────────────────────┘└─────────┘
typ └────┘└────────────────────┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ────────────────────────────────────────┘└─
484 { simp [ht],
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───┘└───────┘└─
485 refine (bot_unique $ infi_le_of_le μ $ _).symm,
id └────────┘ └───────────┘ ┴
src └─────┘ └────────┘┴ ┴└───────────┘┴ ┴ └──────┘
typ └─────┘ └────────┘┴ ┴└───────────┘┴┴┴ └──────┘
doc └─────┘ ┴ ┴ ┴ ┴ └──────┘
txt └─────┘ ┴ ┴ ┴ ┴ └──────┘
par └─────┘ ┴ ┴ ┴ ┴ └──────┘
pid ┴ ┴ ┴ ┴ ┴ └─────┘┴
st ─────────────────────────────────────────────────┘└─
486 refine infi_le_of_le h (le_refl ⊥) },
id └───────────┘ ┴ └─────┘ ┴
src └─────┘└───────────┘┴ ┴ └─────┘┴┴└┘
typ └─────┘└───────────┘┴┴┴ └─────┘┴┴└┘
doc └─────┘ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────┘└┘└
487 { exact Inf_gen_nonempty1 m t ht }
id └───────────────┘ ┴ ┴ └┘
src └────┘└───────────────┘┴ ┴ ┴ ┴
typ └────┘└───────────────┘┴┴┴┴┴└┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
488 end
st ──┘
489
490 lemma Inf_eq_of_function_Inf_gen (m : set (outer_measure α)) :
id └─┘ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ └───────────┘ ┴
491 Inf m = outer_measure.of_function (Inf_gen m) (Inf_gen_empty m) :=
id └─┘ ┴ ┴ └───────────────────────┘ └─────┘ ┴ └───────────┘ ┴
src └─┘ ┴ └───────────────────────┘ └─────┘ └───────────┘
typ └─┘ ┴ ┴ └───────────────────────┘ └─────┘ ┴ └───────────┘ ┴
doc └─┘ └───────────────────────┘
492 begin
st └─────
493 refine le_antisymm
id └─────────┘
src └─────┘└─────────┘└
typ └─────┘└─────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────
494 (assume t', le_of_function.2 (assume t, _) _)
id └────────────┘
src ───┘ └───┘└────────────┘└─┘ └─────────
typ ───┘ └───┘└────────────┘└─┘ └─────────
doc ───┘ └───┘ └─┘ └─────────
txt ───┘ └───┘ └─┘ └─────────
par ───┘ └───┘ └─┘ └─────────
pid ───┘ └───┘ └─┘ └─────────
st ──────────────────────────────────────────────────
495 (lattice.le_Inf $ assume μ hμ t, le_trans (outer_measure.of_function_le _ _ _) _);
id └────────────┘ └──────┘ └──────────────────────────┘
src ───┘ └────────────┘┴ ┴ └───────┘└──────┘┴ └──────────────────────────┘└────────┘
typ ───┘ └────────────┘┴ ┴ └───────┘└──────┘┴ └──────────────────────────┘└────────┘
doc ───┘ ┴ ┴ └───────┘ ┴ └────────┘
txt ───┘ ┴ ┴ └───────┘ ┴ └────────┘
par ───┘ ┴ ┴ └───────┘ ┴ └────────┘
pid ───┘ ┴ ┴ └───────┘ ┴ └────────┘
st ───────────────────────────────────────────────────────────────────────────────────────
496 cases t.eq_empty_or_nonempty with ht ht; simp [ht, Inf_gen_nonempty1],
id └────────────────────┘ └┘ └───────────────┘
src └────┘└────────────────────┘└─────────┘ └────┘ └┘└───────────────┘┴
typ └────┘└────────────────────┘└─────────┘ └────┘└┘└┘└───────────────┘┴
doc └────┘ └─────────┘ └────┘ └┘ ┴
txt └────┘ └─────────┘ └────┘ └┘ ┴
par └────┘ └─────────┘ └────┘ └┘ ┴
pid ┴ └─────────┘ ┴┴ └┘ ┴
st ────────────────────────────────────────────────────────────────────────┘└─
497 { assume μ hμ, exact (show Inf m ≤ μ, from lattice.Inf_le hμ) t },
id └─┘ ┴ ┴ ┴ └────────────┘ └┘ ┴
src └─────────┘ └────┘ ┴└─┘┴ ┴┴┴ └─────┘└────────────┘┴ └┘ ┴
typ └─────────┘ └────┘ ┴└─┘┴┴┴┴┴┴└─────┘└────────────┘┴└┘└┘┴┴
doc └─────────┘ └────┘ ┴└─┘┴ ┴ ┴ └─────┘ ┴ └┘ ┴
txt └─────────┘ └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘ ┴
par └─────────┘ └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘ ┴
pid └─────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └┘ ┴
st ───┘└─────────┘└─────────────────────────────────────────────────┘└┘└
498 { exact infi_le_of_le μ (infi_le _ hμ) }
id └───────────┘ ┴ └─────┘ └┘
src └────┘└───────────┘┴ ┴ └─────┘└─┘ └┘
typ └────┘└───────────┘┴┴┴ └─────┘└─┘└┘└┘
doc └────┘ ┴ ┴ └─┘ └┘
txt └────┘ ┴ ┴ └─┘ └┘
par └────┘ ┴ ┴ └─┘ └┘
pid ┴ ┴ ┴ └─┘ ┴┴
st ────────────────────────────────────────┘└─
499 end
st ──┘
500
501 end Inf_gen
502
503 end outer_measure
504
505 end measure_theory